#include "trier.h"

boolean occur(char* s, char* t) {
    char* temp = malloc(strlen(t) + 1);
    strcpy(temp, t);
    
    boolean flag = false;
    char* pch = strtok(temp, ",().");
    while (pch != NULL) {
        if (strcmp(pch, s) == 0) {
            flag = true;
            break;
        }
        pch = strtok(NULL, ",().");
    }
    
    free(temp);
    return flag;
}

boolean MGU(char* x, char* y) {
    if (strcmp(x,y) == 0) return true;
    else if (isvariable(x)) {
        if (occur(x,y)) return false;
        else {
            unifier[pos][0] = malloc(strlen(x) + 1);
            unifier[pos][1] = malloc(strlen(y) + 1);
            strcpy(unifier[pos][0], x);
            strcpy(unifier[pos][1], y);
            ++pos;
            return true;
        }
    } else if (isvariable(y)) {
        if (occur(y,x)) return false;
        else {
            unifier[pos][0] = malloc(strlen(y) + 1);
            unifier[pos][1] = malloc(strlen(x) + 1);
            strcpy(unifier[pos][0], y);
            strcpy(unifier[pos][1], x);
            ++pos;            
            return true;
        }    
    } else if (isconstant(x) || isconstant(y)) return false;
    else {
        //printf("Here\n");
        printf("%s %s\n",x,y);
        int i=0;
        x = strchr(x,'(') + 1;
        y = strchr(y,'(') + 1;
        *(strrchr(x,')')) = ',';
        *(strrchr(y,')')) = ',';
        
        printf("%s %s\n",x,y);
        while (x[0] != 0) {
            int j,lastmgu=pos;
            char* term1;
            char* term2;
            int k = 0,isi = 0;
            
            while ((x[k] != ',') || isi) {
                if (x[k] == '(') ++isi;
                if (x[k] == ')') --isi;
                ++k;
            }
            
            term1 = malloc(k+1);
            strncpy(term1,x,k);
            term1[k] = 0;
            x += k+1;
            
            k = 0,isi = 0;
            while ((y[k] != ',') || isi) {
                if (y[k] == '(') ++isi;
                if (y[k] == ')') --isi;
                ++k;
            }
            
            term2 = malloc(k+1);
            strncpy(term2,y,k);
            term2[k] = 0;
            y += k+1;            
        
            //printf("%s %s\n",term1,term2);
            boolean hasil = MGU(term1, term2);
            free(term1);
            free(term2);
            if (!hasil) return false;
        
            for (j=lastmgu;j<pos;++j) {
                char* dari = unifier[j][0];
                char* ke = unifier[j][1];
                
                char temp[MaxCol*2];
                memset(temp,0,sizeof(temp));
                int panjang = strlen(x);
                int total = 0,i,j,last = 0;    
                
                for (i=0;i<=panjang;++i) {
                    if (!isalphanum(x[i])) {
                        if (!strcmp(temp + last,dari)) {
                            while (total > last) {
                                temp[--total] = 0;
                            }
                            
                            j=0;
                            while (ke[j]) {
                                temp[total++] = ke[j];
                                ++j;
                            }
                        }
                        last = total+1;
                    }
                    temp[total++] = x[i];
                }
                
                if (strcmp(temp, x)) {
                    free(x);
                    x = malloc(total+1);
                    strcpy(x,temp);
                }
                
                memset(temp,0,sizeof(temp));
                panjang = strlen(y);
                total = 0;last = 0;    
                
                for (i=0;i<=panjang;++i) {
                    if (!isalphanum(y[i])) {
                        if (!strcmp(temp + last,dari)) {
                            while (total > last) {
                                temp[--total] = 0;
                            }
                            
                            j=0;
                            while (ke[j]) {
                                temp[total++] = ke[j];
                                ++j;
                            }
                        }
                        last = total+1;
                    }
                    temp[total++] = y[i];
                }
                
                if (strcmp(temp, y)) {
                    free(y);
                    y = malloc(total+1);
                    strcpy(y,temp);
                }                
            }
        }
        
        return true;
    }
}

void prove_goal(int urut) {
    int i,j,k,l,m,a,b;
    bool done = false;
    
    for (i=2;i<=BBB && !done;++i) {
        for (j=1;j<i && !done;++j) {
            for (k=0;k<member[i] && !done;++k) {
                for (l=0;l<member[j] && !done;++l) {
                    if (positif[i][k] == positif[j][l]) continue;
                    if (isfunction(clauses[i][k]) && isfunction(clauses[j][l])) {
                        m = 0;
                        while (clauses[i][k][m] == clauses[j][l][m] && clauses[i][k][m] != '(') ++m;
                        if (clauses[i][k][m] != '(') continue;
                        char* term1 = malloc(strlen(clauses[i][k])+1);
                        strcpy(term1,clauses[i][k]);
                        char* term2 = malloc(strlen(clauses[j][l])+1);
                        strcpy(term2,clauses[j][l]);
                        
                        boolean hasil = MGU(term1, term2);
                        
                        if (hasil) {
                            
                        }
                        
                        for (m=pos;m>-1;--m) {
                            free(unifier[m][0]);
                            free(unifier[m][1]);
                        }
                        pos = 0;
                        free(term1);
                        free(term2);
                    } else if (isvariable(clauses[i][k]) && isvariable(clauses[j][l])) {
                        if (strcmp(clauses[i][k],clauses[j][l])) continue;
                        ++BBB;
                        member[BBB] = 0;
                        
                        for (a=0;a < member[i];++a) {
                            if (a == k) continue;
                            bool flag = true;
                            for (b=0;b<member[BBB];++b) {
                                if ((positif[BBB][b] == positif[i][a])&&(strcmp(clauses[BBB][b],clauses[i][a]))) {
                                    flag = false;
                                    break;
                                }
                            }
                            
                            if (flag) {
                                positif[BBB][member[BBB]] = positif[i][a];
                                clauses[BBB][member[BBB]] = malloc(strlen(clauses[i][a]) + 1);
                                strcpy(clauses[BBB][member[BBB]],clauses[i][a]);
                                ++member[BBB];
                            }
                        }
                        
                        for (a=0;a < member[j];++a) {
                            if (a == l) continue;
                            bool flag = true;
                            for (b=0;b<member[BBB];++b) {
                                if ((positif[BBB][b] == positif[j][a])&&(strcmp(clauses[BBB][b],clauses[j][a]))) {
                                    flag = false;
                                    break;
                                }
                            }
                            
                            if (flag) {
                                positif[BBB][member[BBB]] = positif[j][a];
                                clauses[BBB][member[BBB]] = malloc(strlen(clauses[j][a]) + 1);
                                strcpy(clauses[BBB][member[BBB]],clauses[j][a]);
                                ++member[BBB];
                            }
                        }             

                        if (!member[BBB]) done = true;
                    } else if (isconstant(clauses[i][k]) && isconstant(clauses[j][l])) {
                        if (strcmp(clauses[i][k],clauses[j][l])) continue;     
                        ++BBB;
                        
                        if (strcmp(clauses[i][k],clauses[j][l])) continue;
                        ++BBB;
                        member[BBB] = 0;
                        
                        for (a=0;a < member[i];++a) {
                            if (a == k) continue;
                            bool flag = true;
                            for (b=0;b<member[BBB];++b) {
                                if ((positif[BBB][b] == positif[i][a])&&(strcmp(clauses[BBB][b],clauses[i][a]))) {
                                    flag = false;
                                    break;
                                }
                            }
                            
                            if (flag) {
                                positif[BBB][member[BBB]] = positif[i][a];
                                clauses[BBB][member[BBB]] = malloc(strlen(clauses[i][a]) + 1);
                                strcpy(clauses[BBB][member[BBB]],clauses[i][a]);
                                ++member[BBB];
                            }
                        }
                        
                        for (a=0;a < member[j];++a) {
                            if (a == l) continue;
                            bool flag = true;
                            for (b=0;b<member[BBB];++b) {
                                if ((positif[BBB][b] == positif[j][a])&&(strcmp(clauses[BBB][b],clauses[j][a]))) {
                                    flag = false;
                                    break;
                                }
                            }
                            
                            if (flag) {
                                positif[BBB][member[BBB]] = positif[j][a];
                                clauses[BBB][member[BBB]] = malloc(strlen(clauses[j][a]) + 1);
                                strcpy(clauses[BBB][member[BBB]],clauses[j][a]);
                                ++member[BBB];
                            }
                        }             

                        if (!member[BBB]) done = true;                        
                    }
                }
            }
        }
    }
}
